$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, $x$:AtomFree(Type$_{\mbox{\scriptsize i}}$;$T$). $x$ $\in$ AtomFree(Type$_{\mbox{\scriptsize i'}}$;$T$)